herbrandscher Satz

herbrandscher Satz

 

[ɛr'brã-], von dem französischen Mathematiker und Logiker Jacques Herbrand (* 1908, ✝ 1931) 1929 bewiesener Satz: Ist A eine Aussage der Prädikatenlogik, so lässt sich eine Disjunktion A₁ ∨. .. ∨ A_n von aussagenlogischen Aussagen konstruieren (»herbrandsche Disjunktion«) mit folgender Eigenschaft: Ist A beweisbar, so auch A₁ ∨. .. ∨ A_n; ist A₁ ∨. .. ∨ A_n beweisbar, so auch A. Der herbrandsche Satz führt also die prädikatenlogische Beweisbarkeit auf die aussagenlogische zurück. Allerdings garantiert er keine Entscheidbarkeit der Prädikatenlogik - was im Widerspruch zum Satz von A. Church stände -, da nicht entscheidbar ist, ob zu gegebenem A überhaupt ein n existiert. Man spricht deshalb auch von Semientscheidbarkeit. Der herbrandsche Satz findet heute u. a. beim automatischen Theorembeweisen im Rahmen der künstlichen Intelligenz Anwendung.